(*
 * Untyped lambda calculus using HOAS.
 *)

datatype exp = lam of (exp -> exp) | app of exp * exp;

fun eval (lam f) = lam (fn x => eval (f x))
  | eval (app (m, n)) =
      case eval m of
        lam f => eval (f n)
      | m => app (m, n)


(* Examples *)

(* lam x. x *)
val id = lam (fn x => x);

(* lam x. lam y. x *)
val k = lam (fn x => lam (fn y => x));

(* The following should evaluate to identity, but we can't check that because
 * SML cannot pattern match on functions, which we are using for our
 * higher-order abstract syntax. *)

eval (app (id, app (app (k, id), k)));
